Modern electronic design automation (EDA) tools are devised to communicate design intent and the circuit behavior between a circuit designer and other technical personnel such as design team member. To facilitate better understanding and more versatility in the applications of these EDA tools, textual and/or graphical interfaces are often provided in these EDA tools so as to enhance the understanding and visualization of various aspects of an electronic design. With the number of transistors in an integrated circuit (IC) doubling approximately every two years according to the Moore's law, contemporary electronic designs have become increasingly bigger and more complex over time.
X-propagation verification is an important area for both simulation and formal verification. Traditionally, ˜$isunknown(s) has been used as a property to be verified for a signal (e.g., signal “s”), optionally modified by the user with a condition to form an expression such as “cond|→˜$isunknown(s)”. Capturing X-behavior or performing X-propagation verification has presented a serious challenge to designers, especially in view of the ever increasingly complex designs. Convention approaches present less than desired or satisfactory solutions in that these conventional approaches for X-propagation verification often require different specifications or representations for different types of nets.
Conventional approaches for X-propagation verification also lack an effective solution to handle a complex design having complex logic elements between the input node and an internal node and also between an internal node and the output node. With such a complex design, conventional approaches lack an effective way to hierarchically decompose the X-propagation verification task into smaller sub-tasks while achieving a satisfactory solution.
Therefore, there exists a need for a method, system, and computer program product for verifying X-behavior in an electronic design to capture X-propagation behavior (or X-behavior) at the net level by extracting precondition and harmless conditions. These techniques described herein may also generate the X-propagation specification for an electronic design or a portion thereof from the RTL (register transfer level) design and use the X-propagation specification for hierarchical verification decomposition. These techniques provide a unified specification for different types of nets and further provide the users with the capabilities to manipulation various aspects of the X-propagation verification.